0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 89 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 37 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 144 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 PiDP
↳9 PiDPToQDPProof (⇔, 76 ms)
↳10 QDP
↳11 QDPOrderProof (⇔, 351 ms)
↳12 QDP
↳13 DependencyGraphProof (⇔, 0 ms)
↳14 QDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 QDP
↳17 QReductionProof (⇔, 0 ms)
↳18 QDP
↳19 UsableRulesReductionPairsProof (⇔, 0 ms)
↳20 QDP
↳21 PisEmptyProof (⇔, 0 ms)
↳22 YES
pA_in_g(cons(T3, nil)) → pA_out_g(cons(T3, nil))
pA_in_g(cons(s(s(s(s(T24)))), cons(T25, T26))) → U1_g(T24, T25, T26, pA_in_g(cons(T24, cons(T25, T26))))
pA_in_g(cons(s(s(0)), cons(T45, T46))) → U4_g(T45, T46, pA_in_g(cons(T45, T46)))
pA_in_g(cons(0, cons(T59, nil))) → pA_out_g(cons(0, cons(T59, nil)))
pA_in_g(cons(0, cons(s(s(T72)), cons(T73, T74)))) → U6_g(T72, T73, T74, pA_in_g(cons(T72, cons(T73, T74))))
pA_in_g(cons(0, cons(0, T83))) → U8_g(T83, pA_in_g(T83))
U8_g(T83, pA_out_g(T83)) → pA_out_g(cons(0, cons(0, T83)))
U6_g(T72, T73, T74, pA_out_g(cons(T72, cons(T73, T74)))) → pA_out_g(cons(0, cons(s(s(T72)), cons(T73, T74))))
U6_g(T72, T73, T74, pA_out_g(cons(T72, cons(T73, T74)))) → U7_g(T72, T73, T74, pA_in_g(cons(s(s(s(s(T73)))), T74)))
U7_g(T72, T73, T74, pA_out_g(cons(s(s(s(s(T73)))), T74))) → pA_out_g(cons(0, cons(s(s(T72)), cons(T73, T74))))
U4_g(T45, T46, pA_out_g(cons(T45, T46))) → pA_out_g(cons(s(s(0)), cons(T45, T46)))
U4_g(T45, T46, pA_out_g(cons(T45, T46))) → U5_g(T45, T46, pA_in_g(cons(s(s(s(s(T45)))), T46)))
U5_g(T45, T46, pA_out_g(cons(s(s(s(s(T45)))), T46))) → pA_out_g(cons(s(s(0)), cons(T45, T46)))
U1_g(T24, T25, T26, pA_out_g(cons(T24, cons(T25, T26)))) → pA_out_g(cons(s(s(s(s(T24)))), cons(T25, T26)))
U1_g(T24, T25, T26, pA_out_g(cons(T24, cons(T25, T26)))) → U2_g(T24, T25, T26, pA_in_g(cons(s(s(s(s(T25)))), T26)))
U2_g(T24, T25, T26, pA_out_g(cons(s(s(s(s(T25)))), T26))) → pA_out_g(cons(s(s(s(s(T24)))), cons(T25, T26)))
U2_g(T24, T25, T26, pA_out_g(cons(s(s(s(s(T25)))), T26))) → U3_g(T24, T25, T26, pA_in_g(cons(s(s(s(s(T25)))), T26)))
U3_g(T24, T25, T26, pA_out_g(cons(s(s(s(s(T25)))), T26))) → pA_out_g(cons(s(s(s(s(T24)))), cons(T25, T26)))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
pA_in_g(cons(T3, nil)) → pA_out_g(cons(T3, nil))
pA_in_g(cons(s(s(s(s(T24)))), cons(T25, T26))) → U1_g(T24, T25, T26, pA_in_g(cons(T24, cons(T25, T26))))
pA_in_g(cons(s(s(0)), cons(T45, T46))) → U4_g(T45, T46, pA_in_g(cons(T45, T46)))
pA_in_g(cons(0, cons(T59, nil))) → pA_out_g(cons(0, cons(T59, nil)))
pA_in_g(cons(0, cons(s(s(T72)), cons(T73, T74)))) → U6_g(T72, T73, T74, pA_in_g(cons(T72, cons(T73, T74))))
pA_in_g(cons(0, cons(0, T83))) → U8_g(T83, pA_in_g(T83))
U8_g(T83, pA_out_g(T83)) → pA_out_g(cons(0, cons(0, T83)))
U6_g(T72, T73, T74, pA_out_g(cons(T72, cons(T73, T74)))) → pA_out_g(cons(0, cons(s(s(T72)), cons(T73, T74))))
U6_g(T72, T73, T74, pA_out_g(cons(T72, cons(T73, T74)))) → U7_g(T72, T73, T74, pA_in_g(cons(s(s(s(s(T73)))), T74)))
U7_g(T72, T73, T74, pA_out_g(cons(s(s(s(s(T73)))), T74))) → pA_out_g(cons(0, cons(s(s(T72)), cons(T73, T74))))
U4_g(T45, T46, pA_out_g(cons(T45, T46))) → pA_out_g(cons(s(s(0)), cons(T45, T46)))
U4_g(T45, T46, pA_out_g(cons(T45, T46))) → U5_g(T45, T46, pA_in_g(cons(s(s(s(s(T45)))), T46)))
U5_g(T45, T46, pA_out_g(cons(s(s(s(s(T45)))), T46))) → pA_out_g(cons(s(s(0)), cons(T45, T46)))
U1_g(T24, T25, T26, pA_out_g(cons(T24, cons(T25, T26)))) → pA_out_g(cons(s(s(s(s(T24)))), cons(T25, T26)))
U1_g(T24, T25, T26, pA_out_g(cons(T24, cons(T25, T26)))) → U2_g(T24, T25, T26, pA_in_g(cons(s(s(s(s(T25)))), T26)))
U2_g(T24, T25, T26, pA_out_g(cons(s(s(s(s(T25)))), T26))) → pA_out_g(cons(s(s(s(s(T24)))), cons(T25, T26)))
U2_g(T24, T25, T26, pA_out_g(cons(s(s(s(s(T25)))), T26))) → U3_g(T24, T25, T26, pA_in_g(cons(s(s(s(s(T25)))), T26)))
U3_g(T24, T25, T26, pA_out_g(cons(s(s(s(s(T25)))), T26))) → pA_out_g(cons(s(s(s(s(T24)))), cons(T25, T26)))
PA_IN_G(cons(s(s(s(s(T24)))), cons(T25, T26))) → U1_G(T24, T25, T26, pA_in_g(cons(T24, cons(T25, T26))))
PA_IN_G(cons(s(s(s(s(T24)))), cons(T25, T26))) → PA_IN_G(cons(T24, cons(T25, T26)))
PA_IN_G(cons(s(s(0)), cons(T45, T46))) → U4_G(T45, T46, pA_in_g(cons(T45, T46)))
PA_IN_G(cons(s(s(0)), cons(T45, T46))) → PA_IN_G(cons(T45, T46))
PA_IN_G(cons(0, cons(s(s(T72)), cons(T73, T74)))) → U6_G(T72, T73, T74, pA_in_g(cons(T72, cons(T73, T74))))
PA_IN_G(cons(0, cons(s(s(T72)), cons(T73, T74)))) → PA_IN_G(cons(T72, cons(T73, T74)))
PA_IN_G(cons(0, cons(0, T83))) → U8_G(T83, pA_in_g(T83))
PA_IN_G(cons(0, cons(0, T83))) → PA_IN_G(T83)
U6_G(T72, T73, T74, pA_out_g(cons(T72, cons(T73, T74)))) → U7_G(T72, T73, T74, pA_in_g(cons(s(s(s(s(T73)))), T74)))
U6_G(T72, T73, T74, pA_out_g(cons(T72, cons(T73, T74)))) → PA_IN_G(cons(s(s(s(s(T73)))), T74))
U4_G(T45, T46, pA_out_g(cons(T45, T46))) → U5_G(T45, T46, pA_in_g(cons(s(s(s(s(T45)))), T46)))
U4_G(T45, T46, pA_out_g(cons(T45, T46))) → PA_IN_G(cons(s(s(s(s(T45)))), T46))
U1_G(T24, T25, T26, pA_out_g(cons(T24, cons(T25, T26)))) → U2_G(T24, T25, T26, pA_in_g(cons(s(s(s(s(T25)))), T26)))
U1_G(T24, T25, T26, pA_out_g(cons(T24, cons(T25, T26)))) → PA_IN_G(cons(s(s(s(s(T25)))), T26))
U2_G(T24, T25, T26, pA_out_g(cons(s(s(s(s(T25)))), T26))) → U3_G(T24, T25, T26, pA_in_g(cons(s(s(s(s(T25)))), T26)))
U2_G(T24, T25, T26, pA_out_g(cons(s(s(s(s(T25)))), T26))) → PA_IN_G(cons(s(s(s(s(T25)))), T26))
pA_in_g(cons(T3, nil)) → pA_out_g(cons(T3, nil))
pA_in_g(cons(s(s(s(s(T24)))), cons(T25, T26))) → U1_g(T24, T25, T26, pA_in_g(cons(T24, cons(T25, T26))))
pA_in_g(cons(s(s(0)), cons(T45, T46))) → U4_g(T45, T46, pA_in_g(cons(T45, T46)))
pA_in_g(cons(0, cons(T59, nil))) → pA_out_g(cons(0, cons(T59, nil)))
pA_in_g(cons(0, cons(s(s(T72)), cons(T73, T74)))) → U6_g(T72, T73, T74, pA_in_g(cons(T72, cons(T73, T74))))
pA_in_g(cons(0, cons(0, T83))) → U8_g(T83, pA_in_g(T83))
U8_g(T83, pA_out_g(T83)) → pA_out_g(cons(0, cons(0, T83)))
U6_g(T72, T73, T74, pA_out_g(cons(T72, cons(T73, T74)))) → pA_out_g(cons(0, cons(s(s(T72)), cons(T73, T74))))
U6_g(T72, T73, T74, pA_out_g(cons(T72, cons(T73, T74)))) → U7_g(T72, T73, T74, pA_in_g(cons(s(s(s(s(T73)))), T74)))
U7_g(T72, T73, T74, pA_out_g(cons(s(s(s(s(T73)))), T74))) → pA_out_g(cons(0, cons(s(s(T72)), cons(T73, T74))))
U4_g(T45, T46, pA_out_g(cons(T45, T46))) → pA_out_g(cons(s(s(0)), cons(T45, T46)))
U4_g(T45, T46, pA_out_g(cons(T45, T46))) → U5_g(T45, T46, pA_in_g(cons(s(s(s(s(T45)))), T46)))
U5_g(T45, T46, pA_out_g(cons(s(s(s(s(T45)))), T46))) → pA_out_g(cons(s(s(0)), cons(T45, T46)))
U1_g(T24, T25, T26, pA_out_g(cons(T24, cons(T25, T26)))) → pA_out_g(cons(s(s(s(s(T24)))), cons(T25, T26)))
U1_g(T24, T25, T26, pA_out_g(cons(T24, cons(T25, T26)))) → U2_g(T24, T25, T26, pA_in_g(cons(s(s(s(s(T25)))), T26)))
U2_g(T24, T25, T26, pA_out_g(cons(s(s(s(s(T25)))), T26))) → pA_out_g(cons(s(s(s(s(T24)))), cons(T25, T26)))
U2_g(T24, T25, T26, pA_out_g(cons(s(s(s(s(T25)))), T26))) → U3_g(T24, T25, T26, pA_in_g(cons(s(s(s(s(T25)))), T26)))
U3_g(T24, T25, T26, pA_out_g(cons(s(s(s(s(T25)))), T26))) → pA_out_g(cons(s(s(s(s(T24)))), cons(T25, T26)))
PA_IN_G(cons(s(s(s(s(T24)))), cons(T25, T26))) → U1_G(T24, T25, T26, pA_in_g(cons(T24, cons(T25, T26))))
PA_IN_G(cons(s(s(s(s(T24)))), cons(T25, T26))) → PA_IN_G(cons(T24, cons(T25, T26)))
PA_IN_G(cons(s(s(0)), cons(T45, T46))) → U4_G(T45, T46, pA_in_g(cons(T45, T46)))
PA_IN_G(cons(s(s(0)), cons(T45, T46))) → PA_IN_G(cons(T45, T46))
PA_IN_G(cons(0, cons(s(s(T72)), cons(T73, T74)))) → U6_G(T72, T73, T74, pA_in_g(cons(T72, cons(T73, T74))))
PA_IN_G(cons(0, cons(s(s(T72)), cons(T73, T74)))) → PA_IN_G(cons(T72, cons(T73, T74)))
PA_IN_G(cons(0, cons(0, T83))) → U8_G(T83, pA_in_g(T83))
PA_IN_G(cons(0, cons(0, T83))) → PA_IN_G(T83)
U6_G(T72, T73, T74, pA_out_g(cons(T72, cons(T73, T74)))) → U7_G(T72, T73, T74, pA_in_g(cons(s(s(s(s(T73)))), T74)))
U6_G(T72, T73, T74, pA_out_g(cons(T72, cons(T73, T74)))) → PA_IN_G(cons(s(s(s(s(T73)))), T74))
U4_G(T45, T46, pA_out_g(cons(T45, T46))) → U5_G(T45, T46, pA_in_g(cons(s(s(s(s(T45)))), T46)))
U4_G(T45, T46, pA_out_g(cons(T45, T46))) → PA_IN_G(cons(s(s(s(s(T45)))), T46))
U1_G(T24, T25, T26, pA_out_g(cons(T24, cons(T25, T26)))) → U2_G(T24, T25, T26, pA_in_g(cons(s(s(s(s(T25)))), T26)))
U1_G(T24, T25, T26, pA_out_g(cons(T24, cons(T25, T26)))) → PA_IN_G(cons(s(s(s(s(T25)))), T26))
U2_G(T24, T25, T26, pA_out_g(cons(s(s(s(s(T25)))), T26))) → U3_G(T24, T25, T26, pA_in_g(cons(s(s(s(s(T25)))), T26)))
U2_G(T24, T25, T26, pA_out_g(cons(s(s(s(s(T25)))), T26))) → PA_IN_G(cons(s(s(s(s(T25)))), T26))
pA_in_g(cons(T3, nil)) → pA_out_g(cons(T3, nil))
pA_in_g(cons(s(s(s(s(T24)))), cons(T25, T26))) → U1_g(T24, T25, T26, pA_in_g(cons(T24, cons(T25, T26))))
pA_in_g(cons(s(s(0)), cons(T45, T46))) → U4_g(T45, T46, pA_in_g(cons(T45, T46)))
pA_in_g(cons(0, cons(T59, nil))) → pA_out_g(cons(0, cons(T59, nil)))
pA_in_g(cons(0, cons(s(s(T72)), cons(T73, T74)))) → U6_g(T72, T73, T74, pA_in_g(cons(T72, cons(T73, T74))))
pA_in_g(cons(0, cons(0, T83))) → U8_g(T83, pA_in_g(T83))
U8_g(T83, pA_out_g(T83)) → pA_out_g(cons(0, cons(0, T83)))
U6_g(T72, T73, T74, pA_out_g(cons(T72, cons(T73, T74)))) → pA_out_g(cons(0, cons(s(s(T72)), cons(T73, T74))))
U6_g(T72, T73, T74, pA_out_g(cons(T72, cons(T73, T74)))) → U7_g(T72, T73, T74, pA_in_g(cons(s(s(s(s(T73)))), T74)))
U7_g(T72, T73, T74, pA_out_g(cons(s(s(s(s(T73)))), T74))) → pA_out_g(cons(0, cons(s(s(T72)), cons(T73, T74))))
U4_g(T45, T46, pA_out_g(cons(T45, T46))) → pA_out_g(cons(s(s(0)), cons(T45, T46)))
U4_g(T45, T46, pA_out_g(cons(T45, T46))) → U5_g(T45, T46, pA_in_g(cons(s(s(s(s(T45)))), T46)))
U5_g(T45, T46, pA_out_g(cons(s(s(s(s(T45)))), T46))) → pA_out_g(cons(s(s(0)), cons(T45, T46)))
U1_g(T24, T25, T26, pA_out_g(cons(T24, cons(T25, T26)))) → pA_out_g(cons(s(s(s(s(T24)))), cons(T25, T26)))
U1_g(T24, T25, T26, pA_out_g(cons(T24, cons(T25, T26)))) → U2_g(T24, T25, T26, pA_in_g(cons(s(s(s(s(T25)))), T26)))
U2_g(T24, T25, T26, pA_out_g(cons(s(s(s(s(T25)))), T26))) → pA_out_g(cons(s(s(s(s(T24)))), cons(T25, T26)))
U2_g(T24, T25, T26, pA_out_g(cons(s(s(s(s(T25)))), T26))) → U3_g(T24, T25, T26, pA_in_g(cons(s(s(s(s(T25)))), T26)))
U3_g(T24, T25, T26, pA_out_g(cons(s(s(s(s(T25)))), T26))) → pA_out_g(cons(s(s(s(s(T24)))), cons(T25, T26)))
U1_G(T24, T25, T26, pA_out_g(cons(T24, cons(T25, T26)))) → U2_G(T24, T25, T26, pA_in_g(cons(s(s(s(s(T25)))), T26)))
U2_G(T24, T25, T26, pA_out_g(cons(s(s(s(s(T25)))), T26))) → PA_IN_G(cons(s(s(s(s(T25)))), T26))
PA_IN_G(cons(s(s(s(s(T24)))), cons(T25, T26))) → U1_G(T24, T25, T26, pA_in_g(cons(T24, cons(T25, T26))))
U1_G(T24, T25, T26, pA_out_g(cons(T24, cons(T25, T26)))) → PA_IN_G(cons(s(s(s(s(T25)))), T26))
PA_IN_G(cons(s(s(s(s(T24)))), cons(T25, T26))) → PA_IN_G(cons(T24, cons(T25, T26)))
PA_IN_G(cons(s(s(0)), cons(T45, T46))) → U4_G(T45, T46, pA_in_g(cons(T45, T46)))
U4_G(T45, T46, pA_out_g(cons(T45, T46))) → PA_IN_G(cons(s(s(s(s(T45)))), T46))
PA_IN_G(cons(s(s(0)), cons(T45, T46))) → PA_IN_G(cons(T45, T46))
PA_IN_G(cons(0, cons(s(s(T72)), cons(T73, T74)))) → U6_G(T72, T73, T74, pA_in_g(cons(T72, cons(T73, T74))))
U6_G(T72, T73, T74, pA_out_g(cons(T72, cons(T73, T74)))) → PA_IN_G(cons(s(s(s(s(T73)))), T74))
PA_IN_G(cons(0, cons(s(s(T72)), cons(T73, T74)))) → PA_IN_G(cons(T72, cons(T73, T74)))
PA_IN_G(cons(0, cons(0, T83))) → PA_IN_G(T83)
pA_in_g(cons(T3, nil)) → pA_out_g(cons(T3, nil))
pA_in_g(cons(s(s(s(s(T24)))), cons(T25, T26))) → U1_g(T24, T25, T26, pA_in_g(cons(T24, cons(T25, T26))))
pA_in_g(cons(s(s(0)), cons(T45, T46))) → U4_g(T45, T46, pA_in_g(cons(T45, T46)))
pA_in_g(cons(0, cons(T59, nil))) → pA_out_g(cons(0, cons(T59, nil)))
pA_in_g(cons(0, cons(s(s(T72)), cons(T73, T74)))) → U6_g(T72, T73, T74, pA_in_g(cons(T72, cons(T73, T74))))
pA_in_g(cons(0, cons(0, T83))) → U8_g(T83, pA_in_g(T83))
U8_g(T83, pA_out_g(T83)) → pA_out_g(cons(0, cons(0, T83)))
U6_g(T72, T73, T74, pA_out_g(cons(T72, cons(T73, T74)))) → pA_out_g(cons(0, cons(s(s(T72)), cons(T73, T74))))
U6_g(T72, T73, T74, pA_out_g(cons(T72, cons(T73, T74)))) → U7_g(T72, T73, T74, pA_in_g(cons(s(s(s(s(T73)))), T74)))
U7_g(T72, T73, T74, pA_out_g(cons(s(s(s(s(T73)))), T74))) → pA_out_g(cons(0, cons(s(s(T72)), cons(T73, T74))))
U4_g(T45, T46, pA_out_g(cons(T45, T46))) → pA_out_g(cons(s(s(0)), cons(T45, T46)))
U4_g(T45, T46, pA_out_g(cons(T45, T46))) → U5_g(T45, T46, pA_in_g(cons(s(s(s(s(T45)))), T46)))
U5_g(T45, T46, pA_out_g(cons(s(s(s(s(T45)))), T46))) → pA_out_g(cons(s(s(0)), cons(T45, T46)))
U1_g(T24, T25, T26, pA_out_g(cons(T24, cons(T25, T26)))) → pA_out_g(cons(s(s(s(s(T24)))), cons(T25, T26)))
U1_g(T24, T25, T26, pA_out_g(cons(T24, cons(T25, T26)))) → U2_g(T24, T25, T26, pA_in_g(cons(s(s(s(s(T25)))), T26)))
U2_g(T24, T25, T26, pA_out_g(cons(s(s(s(s(T25)))), T26))) → pA_out_g(cons(s(s(s(s(T24)))), cons(T25, T26)))
U2_g(T24, T25, T26, pA_out_g(cons(s(s(s(s(T25)))), T26))) → U3_g(T24, T25, T26, pA_in_g(cons(s(s(s(s(T25)))), T26)))
U3_g(T24, T25, T26, pA_out_g(cons(s(s(s(s(T25)))), T26))) → pA_out_g(cons(s(s(s(s(T24)))), cons(T25, T26)))
U1_G(T24, T25, T26, pA_out_g(cons(T24, cons(T25, T26)))) → U2_G(T24, T25, T26, pA_in_g(cons(s(s(s(s(T25)))), T26)))
U2_G(T24, T25, T26, pA_out_g(cons(s(s(s(s(T25)))), T26))) → PA_IN_G(cons(s(s(s(s(T25)))), T26))
PA_IN_G(cons(s(s(s(s(T24)))), cons(T25, T26))) → U1_G(T24, T25, T26, pA_in_g(cons(T24, cons(T25, T26))))
U1_G(T24, T25, T26, pA_out_g(cons(T24, cons(T25, T26)))) → PA_IN_G(cons(s(s(s(s(T25)))), T26))
PA_IN_G(cons(s(s(s(s(T24)))), cons(T25, T26))) → PA_IN_G(cons(T24, cons(T25, T26)))
PA_IN_G(cons(s(s(0)), cons(T45, T46))) → U4_G(T45, T46, pA_in_g(cons(T45, T46)))
U4_G(T45, T46, pA_out_g(cons(T45, T46))) → PA_IN_G(cons(s(s(s(s(T45)))), T46))
PA_IN_G(cons(s(s(0)), cons(T45, T46))) → PA_IN_G(cons(T45, T46))
PA_IN_G(cons(0, cons(s(s(T72)), cons(T73, T74)))) → U6_G(T72, T73, T74, pA_in_g(cons(T72, cons(T73, T74))))
U6_G(T72, T73, T74, pA_out_g(cons(T72, cons(T73, T74)))) → PA_IN_G(cons(s(s(s(s(T73)))), T74))
PA_IN_G(cons(0, cons(s(s(T72)), cons(T73, T74)))) → PA_IN_G(cons(T72, cons(T73, T74)))
PA_IN_G(cons(0, cons(0, T83))) → PA_IN_G(T83)
pA_in_g(cons(T3, nil)) → pA_out_g(cons(T3, nil))
pA_in_g(cons(s(s(s(s(T24)))), cons(T25, T26))) → U1_g(T24, T25, T26, pA_in_g(cons(T24, cons(T25, T26))))
pA_in_g(cons(s(s(0)), cons(T45, T46))) → U4_g(T45, T46, pA_in_g(cons(T45, T46)))
pA_in_g(cons(0, cons(T59, nil))) → pA_out_g(cons(0, cons(T59, nil)))
pA_in_g(cons(0, cons(s(s(T72)), cons(T73, T74)))) → U6_g(T72, T73, T74, pA_in_g(cons(T72, cons(T73, T74))))
pA_in_g(cons(0, cons(0, T83))) → U8_g(T83, pA_in_g(T83))
U8_g(T83, pA_out_g(T83)) → pA_out_g(cons(0, cons(0, T83)))
U6_g(T72, T73, T74, pA_out_g(cons(T72, cons(T73, T74)))) → pA_out_g(cons(0, cons(s(s(T72)), cons(T73, T74))))
U6_g(T72, T73, T74, pA_out_g(cons(T72, cons(T73, T74)))) → U7_g(T72, T73, T74, pA_in_g(cons(s(s(s(s(T73)))), T74)))
U7_g(T72, T73, T74, pA_out_g(cons(s(s(s(s(T73)))), T74))) → pA_out_g(cons(0, cons(s(s(T72)), cons(T73, T74))))
U4_g(T45, T46, pA_out_g(cons(T45, T46))) → pA_out_g(cons(s(s(0)), cons(T45, T46)))
U4_g(T45, T46, pA_out_g(cons(T45, T46))) → U5_g(T45, T46, pA_in_g(cons(s(s(s(s(T45)))), T46)))
U5_g(T45, T46, pA_out_g(cons(s(s(s(s(T45)))), T46))) → pA_out_g(cons(s(s(0)), cons(T45, T46)))
U1_g(T24, T25, T26, pA_out_g(cons(T24, cons(T25, T26)))) → pA_out_g(cons(s(s(s(s(T24)))), cons(T25, T26)))
U1_g(T24, T25, T26, pA_out_g(cons(T24, cons(T25, T26)))) → U2_g(T24, T25, T26, pA_in_g(cons(s(s(s(s(T25)))), T26)))
U2_g(T24, T25, T26, pA_out_g(cons(s(s(s(s(T25)))), T26))) → pA_out_g(cons(s(s(s(s(T24)))), cons(T25, T26)))
U2_g(T24, T25, T26, pA_out_g(cons(s(s(s(s(T25)))), T26))) → U3_g(T24, T25, T26, pA_in_g(cons(s(s(s(s(T25)))), T26)))
U3_g(T24, T25, T26, pA_out_g(cons(s(s(s(s(T25)))), T26))) → pA_out_g(cons(s(s(s(s(T24)))), cons(T25, T26)))
pA_in_g(x0)
U8_g(x0, x1)
U6_g(x0, x1, x2, x3)
U7_g(x0, x1, x2, x3)
U4_g(x0, x1, x2)
U5_g(x0, x1, x2)
U1_g(x0, x1, x2, x3)
U2_g(x0, x1, x2, x3)
U3_g(x0, x1, x2, x3)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
U1_G(T24, T25, T26, pA_out_g(cons(T24, cons(T25, T26)))) → U2_G(T24, T25, T26, pA_in_g(cons(s(s(s(s(T25)))), T26)))
U1_G(T24, T25, T26, pA_out_g(cons(T24, cons(T25, T26)))) → PA_IN_G(cons(s(s(s(s(T25)))), T26))
U4_G(T45, T46, pA_out_g(cons(T45, T46))) → PA_IN_G(cons(s(s(s(s(T45)))), T46))
PA_IN_G(cons(s(s(0)), cons(T45, T46))) → PA_IN_G(cons(T45, T46))
PA_IN_G(cons(0, cons(s(s(T72)), cons(T73, T74)))) → U6_G(T72, T73, T74, pA_in_g(cons(T72, cons(T73, T74))))
PA_IN_G(cons(0, cons(s(s(T72)), cons(T73, T74)))) → PA_IN_G(cons(T72, cons(T73, T74)))
PA_IN_G(cons(0, cons(0, T83))) → PA_IN_G(T83)
POL(0) = 0
POL(PA_IN_G(x1)) = x1
POL(U1_G(x1, x2, x3, x4)) = 1 + x3 + x4
POL(U1_g(x1, x2, x3, x4)) = 1
POL(U2_G(x1, x2, x3, x4)) = 1 + x3
POL(U2_g(x1, x2, x3, x4)) = 1
POL(U3_g(x1, x2, x3, x4)) = 1
POL(U4_G(x1, x2, x3)) = 1 + x2 + x3
POL(U4_g(x1, x2, x3)) = 1
POL(U5_g(x1, x2, x3)) = 1
POL(U6_G(x1, x2, x3, x4)) = 1 + x3
POL(U6_g(x1, x2, x3, x4)) = x4
POL(U7_g(x1, x2, x3, x4)) = 1
POL(U8_g(x1, x2)) = x2
POL(cons(x1, x2)) = 1 + x2
POL(nil) = 0
POL(pA_in_g(x1)) = 1
POL(pA_out_g(x1)) = 1
POL(s(x1)) = 0
pA_in_g(cons(T3, nil)) → pA_out_g(cons(T3, nil))
pA_in_g(cons(s(s(s(s(T24)))), cons(T25, T26))) → U1_g(T24, T25, T26, pA_in_g(cons(T24, cons(T25, T26))))
pA_in_g(cons(s(s(0)), cons(T45, T46))) → U4_g(T45, T46, pA_in_g(cons(T45, T46)))
pA_in_g(cons(0, cons(T59, nil))) → pA_out_g(cons(0, cons(T59, nil)))
pA_in_g(cons(0, cons(s(s(T72)), cons(T73, T74)))) → U6_g(T72, T73, T74, pA_in_g(cons(T72, cons(T73, T74))))
pA_in_g(cons(0, cons(0, T83))) → U8_g(T83, pA_in_g(T83))
U1_g(T24, T25, T26, pA_out_g(cons(T24, cons(T25, T26)))) → pA_out_g(cons(s(s(s(s(T24)))), cons(T25, T26)))
U4_g(T45, T46, pA_out_g(cons(T45, T46))) → pA_out_g(cons(s(s(0)), cons(T45, T46)))
U6_g(T72, T73, T74, pA_out_g(cons(T72, cons(T73, T74)))) → pA_out_g(cons(0, cons(s(s(T72)), cons(T73, T74))))
U8_g(T83, pA_out_g(T83)) → pA_out_g(cons(0, cons(0, T83)))
U6_g(T72, T73, T74, pA_out_g(cons(T72, cons(T73, T74)))) → U7_g(T72, T73, T74, pA_in_g(cons(s(s(s(s(T73)))), T74)))
U7_g(T72, T73, T74, pA_out_g(cons(s(s(s(s(T73)))), T74))) → pA_out_g(cons(0, cons(s(s(T72)), cons(T73, T74))))
U4_g(T45, T46, pA_out_g(cons(T45, T46))) → U5_g(T45, T46, pA_in_g(cons(s(s(s(s(T45)))), T46)))
U5_g(T45, T46, pA_out_g(cons(s(s(s(s(T45)))), T46))) → pA_out_g(cons(s(s(0)), cons(T45, T46)))
U1_g(T24, T25, T26, pA_out_g(cons(T24, cons(T25, T26)))) → U2_g(T24, T25, T26, pA_in_g(cons(s(s(s(s(T25)))), T26)))
U2_g(T24, T25, T26, pA_out_g(cons(s(s(s(s(T25)))), T26))) → pA_out_g(cons(s(s(s(s(T24)))), cons(T25, T26)))
U2_g(T24, T25, T26, pA_out_g(cons(s(s(s(s(T25)))), T26))) → U3_g(T24, T25, T26, pA_in_g(cons(s(s(s(s(T25)))), T26)))
U3_g(T24, T25, T26, pA_out_g(cons(s(s(s(s(T25)))), T26))) → pA_out_g(cons(s(s(s(s(T24)))), cons(T25, T26)))
U2_G(T24, T25, T26, pA_out_g(cons(s(s(s(s(T25)))), T26))) → PA_IN_G(cons(s(s(s(s(T25)))), T26))
PA_IN_G(cons(s(s(s(s(T24)))), cons(T25, T26))) → U1_G(T24, T25, T26, pA_in_g(cons(T24, cons(T25, T26))))
PA_IN_G(cons(s(s(s(s(T24)))), cons(T25, T26))) → PA_IN_G(cons(T24, cons(T25, T26)))
PA_IN_G(cons(s(s(0)), cons(T45, T46))) → U4_G(T45, T46, pA_in_g(cons(T45, T46)))
U6_G(T72, T73, T74, pA_out_g(cons(T72, cons(T73, T74)))) → PA_IN_G(cons(s(s(s(s(T73)))), T74))
pA_in_g(cons(T3, nil)) → pA_out_g(cons(T3, nil))
pA_in_g(cons(s(s(s(s(T24)))), cons(T25, T26))) → U1_g(T24, T25, T26, pA_in_g(cons(T24, cons(T25, T26))))
pA_in_g(cons(s(s(0)), cons(T45, T46))) → U4_g(T45, T46, pA_in_g(cons(T45, T46)))
pA_in_g(cons(0, cons(T59, nil))) → pA_out_g(cons(0, cons(T59, nil)))
pA_in_g(cons(0, cons(s(s(T72)), cons(T73, T74)))) → U6_g(T72, T73, T74, pA_in_g(cons(T72, cons(T73, T74))))
pA_in_g(cons(0, cons(0, T83))) → U8_g(T83, pA_in_g(T83))
U8_g(T83, pA_out_g(T83)) → pA_out_g(cons(0, cons(0, T83)))
U6_g(T72, T73, T74, pA_out_g(cons(T72, cons(T73, T74)))) → pA_out_g(cons(0, cons(s(s(T72)), cons(T73, T74))))
U6_g(T72, T73, T74, pA_out_g(cons(T72, cons(T73, T74)))) → U7_g(T72, T73, T74, pA_in_g(cons(s(s(s(s(T73)))), T74)))
U7_g(T72, T73, T74, pA_out_g(cons(s(s(s(s(T73)))), T74))) → pA_out_g(cons(0, cons(s(s(T72)), cons(T73, T74))))
U4_g(T45, T46, pA_out_g(cons(T45, T46))) → pA_out_g(cons(s(s(0)), cons(T45, T46)))
U4_g(T45, T46, pA_out_g(cons(T45, T46))) → U5_g(T45, T46, pA_in_g(cons(s(s(s(s(T45)))), T46)))
U5_g(T45, T46, pA_out_g(cons(s(s(s(s(T45)))), T46))) → pA_out_g(cons(s(s(0)), cons(T45, T46)))
U1_g(T24, T25, T26, pA_out_g(cons(T24, cons(T25, T26)))) → pA_out_g(cons(s(s(s(s(T24)))), cons(T25, T26)))
U1_g(T24, T25, T26, pA_out_g(cons(T24, cons(T25, T26)))) → U2_g(T24, T25, T26, pA_in_g(cons(s(s(s(s(T25)))), T26)))
U2_g(T24, T25, T26, pA_out_g(cons(s(s(s(s(T25)))), T26))) → pA_out_g(cons(s(s(s(s(T24)))), cons(T25, T26)))
U2_g(T24, T25, T26, pA_out_g(cons(s(s(s(s(T25)))), T26))) → U3_g(T24, T25, T26, pA_in_g(cons(s(s(s(s(T25)))), T26)))
U3_g(T24, T25, T26, pA_out_g(cons(s(s(s(s(T25)))), T26))) → pA_out_g(cons(s(s(s(s(T24)))), cons(T25, T26)))
pA_in_g(x0)
U8_g(x0, x1)
U6_g(x0, x1, x2, x3)
U7_g(x0, x1, x2, x3)
U4_g(x0, x1, x2)
U5_g(x0, x1, x2)
U1_g(x0, x1, x2, x3)
U2_g(x0, x1, x2, x3)
U3_g(x0, x1, x2, x3)
PA_IN_G(cons(s(s(s(s(T24)))), cons(T25, T26))) → PA_IN_G(cons(T24, cons(T25, T26)))
pA_in_g(cons(T3, nil)) → pA_out_g(cons(T3, nil))
pA_in_g(cons(s(s(s(s(T24)))), cons(T25, T26))) → U1_g(T24, T25, T26, pA_in_g(cons(T24, cons(T25, T26))))
pA_in_g(cons(s(s(0)), cons(T45, T46))) → U4_g(T45, T46, pA_in_g(cons(T45, T46)))
pA_in_g(cons(0, cons(T59, nil))) → pA_out_g(cons(0, cons(T59, nil)))
pA_in_g(cons(0, cons(s(s(T72)), cons(T73, T74)))) → U6_g(T72, T73, T74, pA_in_g(cons(T72, cons(T73, T74))))
pA_in_g(cons(0, cons(0, T83))) → U8_g(T83, pA_in_g(T83))
U8_g(T83, pA_out_g(T83)) → pA_out_g(cons(0, cons(0, T83)))
U6_g(T72, T73, T74, pA_out_g(cons(T72, cons(T73, T74)))) → pA_out_g(cons(0, cons(s(s(T72)), cons(T73, T74))))
U6_g(T72, T73, T74, pA_out_g(cons(T72, cons(T73, T74)))) → U7_g(T72, T73, T74, pA_in_g(cons(s(s(s(s(T73)))), T74)))
U7_g(T72, T73, T74, pA_out_g(cons(s(s(s(s(T73)))), T74))) → pA_out_g(cons(0, cons(s(s(T72)), cons(T73, T74))))
U4_g(T45, T46, pA_out_g(cons(T45, T46))) → pA_out_g(cons(s(s(0)), cons(T45, T46)))
U4_g(T45, T46, pA_out_g(cons(T45, T46))) → U5_g(T45, T46, pA_in_g(cons(s(s(s(s(T45)))), T46)))
U5_g(T45, T46, pA_out_g(cons(s(s(s(s(T45)))), T46))) → pA_out_g(cons(s(s(0)), cons(T45, T46)))
U1_g(T24, T25, T26, pA_out_g(cons(T24, cons(T25, T26)))) → pA_out_g(cons(s(s(s(s(T24)))), cons(T25, T26)))
U1_g(T24, T25, T26, pA_out_g(cons(T24, cons(T25, T26)))) → U2_g(T24, T25, T26, pA_in_g(cons(s(s(s(s(T25)))), T26)))
U2_g(T24, T25, T26, pA_out_g(cons(s(s(s(s(T25)))), T26))) → pA_out_g(cons(s(s(s(s(T24)))), cons(T25, T26)))
U2_g(T24, T25, T26, pA_out_g(cons(s(s(s(s(T25)))), T26))) → U3_g(T24, T25, T26, pA_in_g(cons(s(s(s(s(T25)))), T26)))
U3_g(T24, T25, T26, pA_out_g(cons(s(s(s(s(T25)))), T26))) → pA_out_g(cons(s(s(s(s(T24)))), cons(T25, T26)))
pA_in_g(x0)
U8_g(x0, x1)
U6_g(x0, x1, x2, x3)
U7_g(x0, x1, x2, x3)
U4_g(x0, x1, x2)
U5_g(x0, x1, x2)
U1_g(x0, x1, x2, x3)
U2_g(x0, x1, x2, x3)
U3_g(x0, x1, x2, x3)
PA_IN_G(cons(s(s(s(s(T24)))), cons(T25, T26))) → PA_IN_G(cons(T24, cons(T25, T26)))
pA_in_g(x0)
U8_g(x0, x1)
U6_g(x0, x1, x2, x3)
U7_g(x0, x1, x2, x3)
U4_g(x0, x1, x2)
U5_g(x0, x1, x2)
U1_g(x0, x1, x2, x3)
U2_g(x0, x1, x2, x3)
U3_g(x0, x1, x2, x3)
pA_in_g(x0)
U8_g(x0, x1)
U6_g(x0, x1, x2, x3)
U7_g(x0, x1, x2, x3)
U4_g(x0, x1, x2)
U5_g(x0, x1, x2)
U1_g(x0, x1, x2, x3)
U2_g(x0, x1, x2, x3)
U3_g(x0, x1, x2, x3)
PA_IN_G(cons(s(s(s(s(T24)))), cons(T25, T26))) → PA_IN_G(cons(T24, cons(T25, T26)))
No rules are removed from R.
PA_IN_G(cons(s(s(s(s(T24)))), cons(T25, T26))) → PA_IN_G(cons(T24, cons(T25, T26)))
POL(PA_IN_G(x1)) = x1
POL(cons(x1, x2)) = x1 + x2
POL(s(x1)) = x1